i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da), k:Knd, l:IdLnk, tg:Id, n:,
f:(State(ds)Valtype(da;k)da(rcv(l,tg))?Void), es:ES.
source(l) = i
 es-decls(es;i;ds;da)
 (@i[[A;k sends on l with tag tg [s,v.f(s,v)], at marker n]]
 (
 (es-sends-iff2(es;l;tg;da(rcv(l,tg))?Top;ds;e.kind(e) = k
 (& ecl-es-act(es;n;A)(es-init(es;e),e);e.f((state when e),val(e)))) 

latex

Definitions

t  T, P  Q, x:A. B(x), {T}, SQType(T), Id, s = t, Prop, s ~ t, False, A, AB, , {x:A| B(x) }, , Atom$n, es-decls(es;i;ds;da), Type, x. t(x), a:A fp B(a), Knd, ecl(ds;da), IdLnk, Void, rcv(l,tg), KindDeq, x.A(x), f(x)?z, Valtype(da;k), x:AB(x), State(ds), ES, source(l), x:AB(x), P & Q, P  Q, P  Q, Top, ecl-es-act(es;m;x), f(a), es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e)), @i[[x;snd]], x(s1,s2), x,y. t(x;y), k sends on l with tag tg [s,v.f(s;v)], at marker n, x:A. B(x), b, b, , f(x), x  dom(f), Unit, left+right, rec(x.A(x)), e@i. P(e), 1of(t), E, if b t else f fi, Case b of inl(x)  s(x) ; inr(y)  t(y), A & B, sender(e), A/x,y. B(x;y), isrcv(e), loc(e), <a,b>, P  Q, valtype(e), kind(e), val(e), IdDeq, vartype(i;x), state@i, (state when e), es-init(es;e), lnk(e), EqDecider(T), x:A. B(x)

Lemmas

alle-at wf, deq wf, es-lnk wf, es-init wf, es-loc-init, ecl-es-act wf, es-valtype wf, es-kind wf, es-E wf, es-state-when wf, subtype rel dep function, es-loc wf, es-vartype wf, id-deq wf, es-val wf, Knd sq, nat properties, es-isrcv wf, es-sender wf, es-kind-rcv, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, subtype rel self, fpf-ap wf, bool wf, bnot wf, not wf, assert wf, top wf, es-decls-iff, ecl-mng-sends wf, msg-spec1 wf, es-decls wf, lsrc wf, event system wf, decl-state wf, ma-valtype wf, fpf-cap wf, Kind-deq wf, rcv wf, nat wf, IdLnk wf, ecl wf, Knd wf, fpf wf, es-sends-iff-bact, Id wf, Id sq, ecl-mng-sends-single